package javato.activetesting;

import javato.activetesting.activechecker.ActiveChecker;
import javato.activetesting.analysis.AnalysisImpl;
import javato.activetesting.hybridracedetection.HybridRaceTracker;
import javato.activetesting.lockset.LockSet;
import javato.activetesting.lockset.LockSetTracker;
import javato.activetesting.reentrant.IgnoreRentrantLock;
import javato.activetesting.vc.VectorClockTracker;
import javato.activetesting.common.Parameters;

import java.util.TreeSet;
import java.util.TreeMap;

/**
 * Copyright (c) 2007-2008,
 * Koushik Sen    <ksen@cs.berkeley.edu>
 * All rights reserved.
 * <p/>
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 * <p/>
 * 1. Redistributions of source code must retain the above copyright
 * notice, this list of conditions and the following disclaimer.
 * <p/>
 * 2. Redistributions in binary form must reproduce the above copyright
 * notice, this list of conditions and the following disclaimer in the
 * documentation and/or other materials provided with the distribution.
 * <p/>
 * 3. The names of the contributors may not be used to endorse or promote
 * products derived from this software without specific prior written
 * permission.
 * <p/>
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
 * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
 * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
 * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
 * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
 * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
 * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
 * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
 * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
 * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */


public class PAtomicityAnalysis extends AnalysisImpl {
    private VectorClockTracker vcTracker;
    private LockSetTracker lsTracker;
    private IgnoreRentrantLock ignoreRentrantLock;
    private HybridRaceTracker eb;
    private TreeMap<Integer,ThreadInfo> atomicityInfo;

    public void initialize() {
        synchronized (ActiveChecker.lock) {
            vcTracker = new VectorClockTracker();
            lsTracker = new LockSetTracker();
            ignoreRentrantLock = new IgnoreRentrantLock();
            eb = new HybridRaceTracker();
            atomicityInfo = new TreeMap<Integer, ThreadInfo>();
        }
    }

    private ThreadInfo getThreadInfo(Integer thread) {
        ThreadInfo ti = atomicityInfo.get(thread);
        if (ti==null) {
            ti = new ThreadInfo();
            atomicityInfo.put(thread,ti);
        }
        return ti;
    }

    public void lockBefore(Integer iid, Integer thread, Integer lock, Object actualLock) {
        synchronized (ActiveChecker.lock) {
            if (ignoreRentrantLock.lockBefore(thread, lock)) {
                ThreadInfo ti = getThreadInfo(thread);
                LockSet ls = lsTracker.getLockSet(thread);
                Long mem = (long) lock;
                boolean isRead = !ti.isAcquiringAgain(lock);
                eb.checkRace(iid, thread, mem , isRead, vcTracker.getVectorClock(thread), ls,true,false);
                eb.addEvent(iid, thread, mem, isRead, vcTracker.getVectorClock(thread), ls);
                lsTracker.lockBefore(iid, thread, lock);
            }
        }
    }


    public void unlockAfter(Integer iid, Integer thread, Integer lock) {
        synchronized (ActiveChecker.lock) {
            if (ignoreRentrantLock.unlockAfter(thread, lock)) {
                lsTracker.unlockAfter(thread);
                getThreadInfo(thread).lockRelease();
            }
        }
    }

    public void startBefore(Integer iid, Integer parent, Integer child) {
        synchronized (ActiveChecker.lock) {
            vcTracker.startBefore(parent, child);
        }
    }


    public void joinAfter(Integer iid, Integer parent, Integer child) {
        synchronized (ActiveChecker.lock) {
            vcTracker.joinAfter(parent, child);
        }
    }

    public void finish() {
        synchronized (ActiveChecker.lock) {
            eb.dumpRaces();
        }
    }

    class ThreadInfo {
        private int inAtomic = 0;
        private TreeSet<Integer> locksAcquiredOnce = new TreeSet<Integer>();
        private TreeSet<Integer> locksAcquiredTwiceOrMore = new TreeSet<Integer>();

        public void lockRelease() {
            inAtomic--;
            if (inAtomic==0) {
                locksAcquiredOnce.clear();
                locksAcquiredTwiceOrMore.clear();
            }
        }

        public boolean isAcquiringAgain(Integer lock) {
            inAtomic++;
            if (inAtomic>1) {
                if (locksAcquiredTwiceOrMore.contains(lock)) {
                    return true;
                } else if(locksAcquiredOnce.contains(lock)) {
                    locksAcquiredTwiceOrMore.add(lock);
                    return true;
                } else {
                    locksAcquiredOnce.add(lock);
                    return false;
                }
            } else {
                return false;
            }
        }
    }
}
